/*
 * To change this license header, choose License Headers in Project Properties.
 * To change this template file, choose Tools | Templates
 * and open the template in the editor.
 */
grammar SOL_Declarative;

declarative_section : parties_decl  var_decl  input_output_decl  (protocol_incl)*  function_decl 
                    deny_clause*  ((verification_clause)* | EOF) ;

parties_decl : party_line_decl+;
party_line_decl : PARTY ID NEWLINE     //single party definition
				| PARTY (ID COMMA)* ID NEWLINE ;  //multiple party definition
var_decl : var_line_decl+ ;
var_line_decl : DATATYPE (var_list | vector_var_list | matrix_var_list) NEWLINE;

input_output_decl : input_decl+  output_decl+ ;
input_decl : ID COLON INPUT_KEYWORD var_list NEWLINE;
output_decl : ID COLON OUTPUT_KEYWORD var_list NEWLINE;

protocol_incl : (PROTOCOL_KEYWORD ID LB (arg_list)* RB NEWLINE)+;

function_decl: ((ID COLON)? FUNCTION_KEYWORD  ID LB (arg_list)* RB NEWLINE)+;

deny_clause : DENY_KEYWORD ID ':' var_list NEWLINE;

verification_clause : VERIFICATION_KEYWORD ID COLON ID LB var_list RB (NEWLINE|EOF);

var_list : (ID COMMA)* ID;
vector_var_list : var_list | ((ID LB (ID | INT)  RB COMMA)* (ID LB (ID | INT) RB));
matrix_var_list : var_list | ((ID LB (ID | INT) COMMA (ID | INT) RB COMMA)* (ID LB (ID | INT) COMMA (ID | INT) RB));
arg_list : (DATATYPE ID COMMA)* DATATYPE ID;

PARTY : 'Client' | 'client' | 'Cloud' | 'cloud';
DATATYPE : SIMPLE_DATATYPE | VECTOR_DATATYPE | MATRIX_DATATYPE;
SIMPLE_DATATYPE : 'Val' | 'HVal' | 'GVal' | 'int' ;
VECTOR_DATATYPE : 'Vector' | 'HVector' | 'GVector';
MATRIX_DATATYPE : 'Matrix' | 'HMatrix' | 'GMatrix';
INPUT_KEYWORD : 'Input' | 'input';
OUTPUT_KEYWORD : 'Output' | 'output';
PROTOCOL_KEYWORD: 'Protocol' | 'protocol';
DENY_KEYWORD : 'Deny' | 'deny';
FUNCTION_KEYWORD: 'Function' | 'function';
VERIFICATION_KEYWORD : 'Verification';
ID : (('a'..'z' | 'A'..'Z')+ (INT|UNDER_SCORE)*)+;
INT : '0'..'9'+; 
COLON : ':';
LB : '(';
RB : ')';
COMMA : ',';
UNDER_SCORE : '_';
WS  :   (' '|'\t')+ {skip();} ;
NEWLINE : '\r'? '\n';